\begin{tabbing}
f2f+{-}pred\=\{i:l\}\+
\\[0ex](${\it es}$; ${\it ff}$; ${\it f2f+}$; ${\it sndr}$; ${\it rcvr}$; ${\it e'}$; $e$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=(snd{-}it(${\it ff}$; f2f+Req(${\it f2f+}$); $e$; ${\it sndr}$; ${\it rcvr}$)\+
\\[0ex]$\wedge$ ($\exists$\=$a$:es{-}E(${\it es}$)\+
\\[0ex](($a$ c$\leq$ $e$ $\wedge$ rcv{-}it(${\it ff}$; f2f+Ack(${\it f2f+}$); $a$; ${\it sndr}$; ${\it rcvr}$))
\\[0ex]$\wedge$ \=($\forall$$x$:es{-}E(${\it es}$). \+
\\[0ex](es{-}causl(${\it es}$; $a$; $x$) $\wedge$ $x$ c$\leq$ $e$) $\Rightarrow$ ($\neg$rcv{-}it(${\it ff}$; f2f+Ack(${\it f2f+}$); $x$; ${\it sndr}$; ${\it rcvr}$)))
\-\\[0ex]$\wedge$ (${\it e'}$ = fifoSender(${\it ff}$)(${\it sndr}$,$a$)))))
\-\\[0ex]$\vee$ \=(snd{-}it(${\it ff}$; f2f+Ack(${\it f2f+}$); $e$; ${\it rcvr}$; ${\it sndr}$)\+
\\[0ex]$\wedge$ ($\exists$\=$a$:es{-}E(${\it es}$)\+
\\[0ex](($a$ c$\leq$ $e$ $\wedge$ rcv{-}it(${\it ff}$; f2f+Req(${\it f2f+}$); $a$; ${\it rcvr}$; ${\it sndr}$))
\\[0ex]$\wedge$ \=($\forall$$x$:es{-}E(${\it es}$). \+
\\[0ex](es{-}causl(${\it es}$; $a$; $x$) $\wedge$ $x$ c$\leq$ $e$) $\Rightarrow$ ($\neg$rcv{-}it(${\it ff}$; f2f+Req(${\it f2f+}$); $x$; ${\it rcvr}$; ${\it sndr}$)))
\-\\[0ex]$\wedge$ (${\it e'}$ = fifoSender(${\it ff}$)(${\it rcvr}$,$a$)))))
\-\-\-
\end{tabbing}